A:Type, B:(AType), eq:EqDecider(A), f, g:a:A fp B(a), x:A, P:(a:AB(a)Prop).
g  f  (z != f(x)  P(x,z))  (z != g(x)  P(x,z)) 

latex

Definitions	P  Q, A & B, x:A. B(x), t  T, EqDecider(T), x(s), x. t(x), a:A fp B(a), Prop, Top, f(x), x  dom(f), b, x(s1,s2), z != f(x)  P(a;z), f  g
Lemmas	assert wf, fpf-dom wf, fpf-ap wf, fpf-trivial-subtype-top, fpf wf, deq wf